// Convert a JavaScript Date object into an RFC822-formatted string.
function dateToRFC822(date) {
    function padWithZero(val) {
        return (parseInt(val) < 10) ? ("0" + val) : val;
    }
    
    function offsetStr(offset) {
        if (offset == 0) {
            return "GMT";
        } else {
            var hours = Math.floor(offset / 60);
            var minutes = Math.abs(offset % 60);
            var s = (hours > 0) ? "-" : "+";
            var absHours = Math.abs(hours);
            s += padWithZero(absHours) + ((minutes == 0) ? "00" : minutes);
            return s;
        }
    }
    
    var months = [ "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug",
                   "Sep", "Oct", "Nov", "Dec" ];
    var days = [ "Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat" ];
    
    return days[date.getDay()] + ", " + padWithZero(date.getDate()) + " " +
        months[date.getMonth()] + " " + date.getFullYear() + " " +
        padWithZero(date.getHours()) + ":" +
        padWithZero(date.getMinutes()) + ":" +
        padWithZero(date.getSeconds()) + " " +
        offsetStr(date.getTimezoneOffset());
}

// Return the array of strings with prefix appended to each.
function addPrefix(prefix, strings) {
    var result = [];
    for (var i = 0, s; s = strings[i]; ++i) {
        result[result.length] = prefix + s;
    }
    return result;
}

// Return true if an element with the specified ID exists.
function elementExists(id) {
    return (document.getElementById(id) != null);
}
